Step of Proof: integer sqrt 11,40

Inference at * 1 0 1 2 
Iof proof for Lemma integer sqrt:

.....basecase..... NILNIL

  (0  0 )  (r:. (((r * r 0) & (0 < ((r+1) * (r+1))))) 
latex

 by D 0 
latex


 1

 1: 1. 0  0 
 1:   r:. (((r * r 0) & (0 < ((r+1) * (r+1))))
 2: .....wf..... NILNIL

 2:   (0  0 )  
 .


Definitionsx:A  B(x), a < b, A  B, , x:AB(x), i  j , P  Q, x:AB(x), P & Q, t  T,
Lemmasle wf, nat wf, ge wf

origin